x:. |x|   

latex

Definitions	True, T, ff, P  Q, P & Q, , P  Q, tt, P  Q, if b then t else f fi , |x|, , t  T, x:A. B(x), Unit, ,
Lemmas	assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, bnot wf, le wf, le int wf, assert of lt int, eqtt to assert, assert wf, iff transitivity, bool wf, lt int wf